; <lemma>
;  <title>ch915_maxi.7</title>
;  <origin>ch915_maxi | maxi_1 | inc/inv4/INV</origin>
(benchmark ch915_maxi_7
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="p" type="INTEGER"/>
;    <variable name="q" type="INTEGER"/>
;  </typenv>
  :extrafuns ((p Int)
	       (q Int))
  :extramacros (
		 (singleton (lambda (?x 't) . (lambda (?y 't) . (= ?x ?y))))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 (union
		   (lambda (?p1 ('t boolean)) (?q1 ('t boolean)) .
		     (lambda (?x 't) . (or (?p1 ?x) (?q1 ?x)))))
		 )
; <hypothesis needed="true">p &lt; q</hypothesis>
  :assumption (< p q)
; <goal>p .. q = p+1 .. q \/ {p}</goal>
  :formula
  (not
      (= (range p q) (union (range (+ p 1) q) (singleton p)))
    )
)
; </lemma>

